Nuprl Lemma : ma-x-equiv-read-state
11,40
postcript
pdf
M
:MsgA,
x
:Id,
s1
,
s2
:
M
.(timed)state.
ma-x-tequiv(
M
;
x
;
s1
;
s2
)
(read-state(
s1
)
read-state(
s2
) mod
x
)
latex
Definitions
MsgA
,
t
T
,
Id
,
x
:
A
.
B
(
x
)
,
M
.ds(
x
)
,
,
x
:
A
B
(
x
)
,
f
(
a
)
,
s
=
t
,
,
A
,
P
Q
,
<
a
,
b
>
,
timedState(
ds
)
,
(
s1
s2
mod
x
)
,
read-state(
s
)
,
ma-x-tequiv(
M
;
x
;
s1
;
s2
)
,
M
.(timed)state
,
,
#$n
,
s
~
t
,
{
T
}
,
SQType(
T
)
Lemmas
int
inc
rationals
,
not
wf
,
rationals
wf
,
ma-ds
wf
,
Id
wf
,
msga
wf
origin
M:MsgA, x:Id, s1, s2:M.(timed)state.
(read-state(s1) 
read-state(s2) mod x) M:MsgA, x:Id, s1, s2:M.(timed)state.
(read-state(s1) read-state(s2) mod x) 
Tx:A. B(x)
B(x)
A Q s2 mod x)